This paper introduces an extension A of Kleene's axiomatization of Brouwer's intuitionistic analysis, in which the classical arithmetical and analytical hierarchies are faithfully represented as hierarchies of the domains of continuity. A domain of continuity is a relation R(α) on Baire space with the property that every constructive partial functional defined on {α : R(α)} is continuous there. The domains of continuity for A coincide with the stable relations (those equivalent in A to their double negations), while every relation R(α) (...) is equivalent in A to ∃αA(α, β) for some stable A(α, β) (which belongs to the classical analytical hierarchy). The logic of A is intuitionistic. The axioms of A include countable comprehension, bar induction, Troelstra's generalized continuous choice, primitive recursive Markov's Principle and a classical axiom of dependent choices proposed by Krauss. Constructive dependent choices, and constructive and classical countable choice, are theorems, A is maximal with respect to classical Kleene function realizability, which establishes its consistency. The usual disjunction and (recursive) existence properties ensure that A preserves the constructive sense of "or" and "there exists.". (shrink)

In the author's Relative lawlessness in intuitionistic analysis [this JOURNAL. vol. 52 (1987). pp. 68-88] and An intuitionistic theory of lawlike, choice and lawless sequences [Logic Colloquium '90. Springer-Verlag. Berlin. 1993. pp. 191-209] a notion of lawless ness relative to a countable information base was developed for classical and intuitionistic analysis. Here we simplify the predictability property characterizing relatively lawless sequences and derive it from the new axiom of closed data (classically equivalent to open data) together with a natural principle (...) of invariance under finite translation. We characterize relative lawlessness in terms of a notion of forcing. Finally, we study relative lawlessness on an arbitrary fan and show that the collection of lawless binary sequences (which is comeager in the sense of Baire) has probability measure zero. The reasoning is predominantly constructive. (shrink)

Kripke recently suggested viewing the intuitionistic continuum as an expansion in time of a definite classical continuum. We prove the classical consistency of a three-sorted intuitionistic formal system IC, simultaneously extending Kleene’s intuitionistic analysis I and a negative copy C° of the classically correct part of I, with an “end of time” axiom ET asserting that no choice sequence can be guaranteed not to be pointwise equal to a definite sequence. “Not every sequence is pointwise equal to a definite sequence” (...) is independent of IC. The proofs are by Crealizability interpretations based on classical ω-models ${\cal M}$ = $\left$ of C°. (shrink)

This paper introduces, as an alternative to the (absolutely) lawless sequences of Kreisel and Troelstra, a notion of choice sequence lawless with respect to a given class D of lawlike sequences. For countable D, the class of D-lawless sequences is comeager in the sense of Baire. If a particular well-ordered class F of sequences, generated by iterating definability over the continuum, is countable then the F-lawless, sequences satisfy the axiom of open data and the continuity principle for functions from lawless (...) to lawlike sequences, but fail to satisfy Troelstra's extension principle. Classical reasoning is used. (shrink)

This note explores the common core of constructive, intuitionistic, recursive and classical analysis from an axiomatic standpoint. In addition to clarifying the relation between Kleene’s and Troelstra’s minimal formal theories of numbers and number-theoretic sequences, we propose some modified choice principles and other function existence axioms which may be of use in reverse constructive analysis. Specifically, we consider the function comprehension principles assumed by the two minimal theories EL and M, introduce an axiom schema CFd asserting that every decidable property (...) of numbers has a characteristic function, and use it to describe a precise relationship between the minimal theories. We show that the axiom schema AC00 of countable choice can be decomposed into a monotone choice schema AC00m (which guarantees that every Cauchy sequence has a modulus) and a bounded choice schema BC00. We relate various (classically correct) axiom schemas of continuous choice to versions of the bar and fan theorems, suggest a constructive choice schema AC1/2,0 (which incidentally guarantees that every continuous function has a modulus of continuity), and observe a constructive equivalence between restricted versions of the fan theorem and correspondingly restricted bounding axioms \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${AB_{1/2,0}^{2^{\mathbb{n}}}}$$\end{document}. We also introduce a version WKL!! of Weak König’s Lemma with uniqueness which is intermediate in strength between WKL and the decidable fan theorem FTd. (shrink)

Realizabilities are powerful tools for establishing consistency and independence results for theories based on intuitionistic logic. Troelstra discovered principles ECT 0 and GC 1 which precisely characterize formal number and function realizability for intuitionistic arithmetic and analysis, respectively. Building on Troelstra's results and using his methods, we introduce the notions of Church domain and domain of continuity in order to demonstrate the optimality of “almost negativity” in ECT 0 and GC 1 ; strengthen “double negation shift” DNS 0 to DNS (...) 1 and use it with GC 1 and Markov's Principle MP to characterize the classically provably realizable formulas of analysis; and show that intuitionistic analysis with GC 1 , MP and DNS 1 is consistent and satisfies Troelstra's and Church's Rules. We end with a discussion of semi-intuitionistic theories and a conjecture. (shrink)